Integrated circuits (ICs) have become the backbone of modern consumer electronics. The increased demand for functionality of consumer electronics has forced the complexity of IC's to skyrocket. In a number of applications, ICs must be highly functional, low cost and have low power consumption. These demands create increased complexity on the design, verification, and manufacture of ICs.
A typical IC design may involve the creation of electronic components, such as transistors and resistors, and the interconnections of these components onto a substrate, such as silicon. The simulation, verification, and sometimes layout of these components usually is accomplished in sub-blocks, or modules. Each block may be simulated and verified individually. Multiple design teams typically work on the individual blocks. During the design process functional verification is critical.
Functional verification involves the verification that the design conforms to the specification. It additionally may involve the validation that a design meets the desired functionality. Part of the process of verification includes the creation of Register Transfer Level (RTL) digital designs that describe in detail the functionality of the device or block at every cycle of the clock. Creation and verification RTL design may be one of the more difficult portions of the design process. In many instances, this verification is a very difficult and time intensive task. Simulation tools are typically used to assist in verification. In most designs, simulation-based functional verification is performed on multiple machines in parallel. The process is processor and memory intensive and presents significant difficulties and expenses in the design process.
The satisfiability problem (SAT) is ubiquitous in EDA applications. It is used in equivalence checking, logic synthesis, test generation, model checking to name a few. There are a number of computer aided techniques that are typically used to verify the functionality of digital designs. For example, model checking is a widely used formal verification technique that may be implemented with Binary Decision Diagrams (BDD). As is known in the art, BDDs are data structures used to represent Boolean functions. With recent advances in tools to solve the Boolean satisfiability problem (SAT), SAT solvers are proving to be an effective alternative to BDD's. A given Boolean formula is considered satisfiable if all the variables in the formula can take on such values to make the formula evaluate to true. Alternatively, and potentially more important, if no combination of values can be found that forces the function to evaluate to true, then the formula is unsatisfiable. With complex digital designs, verification approaches can be significantly complex and the memory limits of a computer can be quickly reached.
The most successful SAT-solvers are based on the Davis Putnam Logemann Loveland (DPLL) procedure. In turn, this procedure is based on branching on the values of variables of the CNF formula F to be solved. The process of picking the next assignment of a variable of F is called decision-making. Efficient and effective decision-making is very important for the success of SAT-solvers based on the DPLL procedure. Currently, SAT-solvers use variations of conflict driven decision making introduced by the SAT-solver Chaff.
The general DPLL procedure involves three basic parts, decide, deduce, and analyze conflict. In the decision phase, assignments are made to literals of a CNF formula. In the deduce phase, also referred to as Boolean Constraint Propagation (BCP), clauses are evaluated based on the assignments made. If conflicts are found they are reported. When a unit clause is identified, the unit literal is forced to true. If there is an earlier assignment to this variable, an intersection of the variable value set and the unit literal value set provides the final implication assignment. If no further implications can be derived deduce reports success. The analyze conflict phase identifies the assignments causing conflict and adds a clause to the formula which represents an abstraction of unsatisfiable parts of the solution space. The added clause is referred to as a conflict-induced clause, or a learned clause. The process of constructing the learned clauses is known as conflict-based learning. A conflict is resolved by backtracking. Backtracking undoes all recent assignments up to the most recent decision responsible for the conflict. In many cases not all decisions made so far are responsible for the conflict. In these cases it is possible to backtrack beyond one decision level. This is referred to as non-chronological backtracking. If the conflict cannot be resolved, i.e., all decision assignments will cause a conflict, analyze conflict reports failure.
Resolution based SAT-solvers have gained great popularity due to their ability to solve very large practical CNF formulas. An important contributor to this success is conflict driven decision making (CDDM) introduced initially in “Chaff: Engineering an Efficient SAT Solver”, M. Moskewicz, C. Madigan, Y Zhou, L. Zhang, S. Malik, DAC-2001. A number of others have provided advancements in this space including “BerkMin: a Fast and Robust SAT-Solver”, E. Goldberg, DATE-2002, Paris, pp-142-149; “An Extensible SAT-solver.” E. Sorensson, Proceedings of SAT-2003 in LNCS 2919, pp 503-518. CDDM takes into account the history of conflicts thus forcing the SAT-solver to explore parts of the search space that have not been visited before. Despite the obvious success of CDDM, still there are many directions to explore.
Currently there are two approaches to SAT-solving. One approach is local search algorithms. These algorithms operate on complete assignments and are usually applicable only to satisfiable formulas. The advantage of a local search algorithm is that it ‘knows’ exactly what clauses of the formula are left falsified (i.e. unsatisfied). To reach a satisfying assignment a local search algorithm flips values of variables trying to get a new complete assignment that falsifies fewer clauses.
Another approach is SAT-solvers based on the DPLL procedure. A DPLL-based SAT-solver maintains a partial assignment trying to extend it (one variable assignment at a time) to satisfy all the clauses. If a clause, become unsatisfiable, such a SAT-solver backtracks and changes some variable assignment. A DPLL-based SAT-solvers can be used for both satisfiable and unsatisfiable formulas. The advantage of these SAT-solvers is that they employ Boolean Constraint Propagation (BCP) and clause learning. BCP is used to make ‘forced’ assignments (if an unsatisfied clause has only one literal left unassigned, there is only one way to satisfy this clause). Clause learning allows DPLL-based SAT-solvers to introduce new implications that make BCP more powerful.
The main flaw of local search algorithms is that they do not work well on structured formulas (for example, formulas that describe circuits). The reason is that these algorithms do not use BCP and learning.
The drawbacks of DPLL-based SAT-solvers are as follows. Since these SAT-solvers maintain only a partial assignment they do not ‘know’ how many clauses of the formula are currently falsified. So such a SAT-solver can get very close to a satisfying assignment not being able to benefit from this proximity. The fact that a DPLL-based SAT-solver maintains only a partial assignment also deteriorates this SAT-solver's decision making for unsatisfiable formulas. If for example, a CNF formula has a small unsatisfiable subformula, a DPLL based SAT-solver may never ‘reach’ this subformula.
Another method combines local search and a DPLL-based procedure. This method, “FI” maintains a partial and a complete assignment. The idea of FI is to reduce branching choices to the variables of clauses that are falsified by the current complete assignment. FI maintains a complete and partial assignments, which mitigates the problems that DPLL-based SAT-solvers have. Nevertheless, FI still has the following flaws. Since FI maintains a complete assignment it knows what clauses of the formula are currently falsified. However, it has no ability to reduce the number of falsified clauses as it is done by local search algorithms.
As far as unsatisfiable formulas are concerned, FI has the following drawback. Suppose that the formula F to be solved contains a small unsatisfiable subformula F′. No matter how one picks a complete assignment, a clause of F′ is falsified by this assignment. FI maintains a complete assignment w and limits the choice of next branching variable only to the variables of clauses falsified by w. So a variable of F′ will be always available to FI for branching. Ideally, one would like w to falsify only clauses of F′ (branching in variables of F′ leads to quick solving the formula F). However, in reality, w falsifies a lot of clauses of F that are not in F′. This reduces the chances of FI to pick a variable of F′ for branching.
Therefore there exists a need for a system, and methods for improved SAT-solvers.